es:ES, k:Knd, T:Type, l:IdLnk, ds, dt:x:Id fp Type,
g:(tg:Id(State(ds)T(dt(tg)?Void List))) List.
sends k(v:T) on l:tagged(g,State(ds),v):dt  Prop 

latex

Definitions

Id, f(x)?z, t  T, x:A. B(x), x. t(x), Top, a:A fp B(a), P  Q, tag(e), IdDeq, x  dom(f), b, lnk(e), IdLnk, P & Q, isrcv(e), A & B, E, S  T, rcvs from e on l = L, x:A. B(x), valtype(e), kind(e), Knd, source(l), loc(e), e@i. P(e), vartype(i;x), Prop, sends k(v:T) on l:tagged(g,State(ds),v):dt, ES, State(ds), P  Q, (x  l), P  Q, xL. P(x), P  Q, ||as||, False, A, AB, , True, T, SqStable(P), val(e), map(f;as), b, , f(x), Unit, state@i, (state when e), sends-msgs(s;v;tg_f), concat(ll)

Lemmas

concat wf, sends-msgs wf, es-state-when wf, subtype rel dep function, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, subtype rel self, fpf-ap wf, bool wf, bnot wf, not wf, map wf, es-val wf, sq stable and, sq stable from decidable, decidable assert, cons member, list-set-type2, l member wf, decl-state wf, fpf wf, event system wf, es-vartype wf, fpf-cap wf, top wf, es-loc wf, lsrc wf, Knd wf, es-kind wf, es-valtype wf, es-rcv-from wf, es-E wf, es-isrcv wf, IdLnk wf, es-lnk wf, assert wf, fpf-dom wf, id-deq wf, es-tag wf, fpf-trivial-subtype-top, Id wf